T:Type, L:(T List), R:({x:T| (x  L)} {x:T| (x  L)} ).
Trans({x:T| (x  L)} ;x,y.R(x,y))
 (i:{0..(||L|| - 1)}. R(L[i],L[(i+1)]))
 (((null(L)))  R(last(L),hd(L)))
 (aL. bL. R(a,b)) 

latex

Definitions	t  T, x:A. B(x), #$n, ||as||, n+m, i  j , b, True, False, P  Q, A, type List, x:AB(x), f(a), x(s1,s2), xL. P(x), hd(l), Type, , x,y. t(x;y), Trans(T;x,y.E(x;y)), P & Q, i  j < k, -n, n - m, a < b, A  B, , {i..j}, Void, l[i], x:A.B(x), Top, last(L), S  T, null(as), (x  l), {x:A| B(x)} , s = t
Lemmas	l member-set, not wf, assert wf, null wf3, top wf, last wf, hd wf, int seg wf, select wf, trans wf, transitive-loop, l member wf, non neg length, length wf1, list-subtype